Nuprl Lemma : mk_dset_wf
13,42
postcript
pdf
T
:Type,
eq
:(
T
T
). IsEqFun(
T
;
eq
)
(mk_dset(
T
,
eq
)
DSet)
latex
Up
sets
1
Definitions of Statement
PosetSig
,
|
p
|
,
=
,
DSet
,
mk_dset(
T
,
eq
)
Definitions
mk_dset(
T
,
eq
)
,
DSet
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
PosetSig
,
t
.2
,
t
.1
,
=
,
|
p
|
,
Lemmas
bool
wf
,
set
eq
wf
,
set
car
wf
,
eqfun
p
wf
origin
T:Type, eq:(T
T
). IsEqFun(T;eq) 
(mk_dset(T, eq) 
DSet) T:Type, eq:(TT). IsEqFun(T;eq) (mk_dset(T, eq) DSet) 
T Qx:A. B(x)